Nuprl Lemma : cless_wf
0,22
postcript
pdf
E
,
X1
,
X2
:Type,
info
:(
E
(Id
X1
+(IdLnk
E
)
X2
)),
pred?
:(
E
(
E
+Unit)),
e
,
e'
:
E
.
e
<
e'
Prop
latex
Definitions
e
<
e'
,
R
^+
,
pred!(
e
;
e'
)
,
x
:
A
.
B
(
x
)
,
Unit
,
Id
,
IdLnk
,
t
T
Lemmas
IdLnk
wf
,
Id
wf
,
unit
wf
,
pred!
wf
,
rel
plus
wf
origin
E, X1, X2:Type, info:(E
(Id
X1+(IdLnkE)X2)), pred?:(E(E+Unit)), e, e':E. e < e' 
Prop E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), pred?:(E(E+Unit)), e, e':E. e < e' Prop x:A. B(x) T